ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple{i:l}(ds; da), n:.
(ecl-trans-act(ds; da; A)(n,[]))  False 

latex

Definitions	False, prop{i:l}, x. t(x), t  T, P  Q, P  Q, P  Q, P  Q, x:A. B(x), P  Q, decidable(P), x(s), x:A. B(x), ecl-trans-act(ds; da; A)
Lemmas	decidable false, Id wf, Knd wf, fpf wf, ecl-trans-tuple wf, nat wf, false wf, event-info wf, ecl-trans-act wf, append is nil